Inference at * 2 
Iof proof for Lemma quot elim:



1. T : Type
2. E : TT
3. EquivRel(T;x,y.E(x,y))
4. a : T
5. b : T
6. E(a,b)
  a = b 

latex

 by D 6 

latex

 1: 

 1: 6. E(a,b)
 1:   a = b
 .

Definitions

T